Issue1388.agda:7,1-19
No declarations allowed after top-level module.
